Nuprl Lemma : wellfounded_functionality_wrt_iff 13,42
T1, T2:Type, r1:(T1T1), r2:(T2T2).
(T1 = T2)
 (x, y:T1. r1(x,y)  r2(x,y))
 (WellFnd{i}(T1;x,y.r1(x,y))  WellFnd{i}(T2;x,y.r2(x,y))) 
latex

Upwell fnd, well fnd
DefinitionsP  Q, P & Q, t  T, x(s1,s2), P  Q, P  Q, , x:A. B(x), x,y. t(x;y), {T}
Lemmasiff wf, wellfounded functionality wrt implies

origin